$\forall$$A$, $B$:MsgA, $x$:Id.
\\[0ex]$A$ $\parallel$ $B$
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd, $s$:$A$.state, $v$:$A$.da($k$). ma{-}ef{-}const($A$;$k$;$x$;$s$;$v$))
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd, $s$:$B$.state, ${\it v@}_{0}$:$B$.da($k$). ma{-}ef{-}const($B$;$k$;$x$;$s$;${\it v@}_{0}$))
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd, $s$:$A$ $\oplus$ $B$.state, $v$:$A$ $\oplus$ $B$.da($k$). ma{-}ef{-}const($A$ $\oplus$ $B$;$k$;$x$;$s$;$v$))